R:Realizer, es:ES.
(i, x:Id. (<i, x>  dom(R-discrete(R)))  (R-discrete(R)(<i, x>) = discrete(i;x)  ))
 Possible(R;es)
 Consistent(R;es) 

latex

Definitions

suptype(S; T), S  T, State(ds), a = b, R-base-ma(R), R-loc(R), @i: A, case(R)Rnone: noneleft  right: comb(left;right)base(b). base(b), [[R]], SQType(T), if b then t else f fi , P  Q, tt, {T}, Top, , @i: only members of L read x, @i:k sends only on links in L, @i continuous x initially v:T, P & Q, True, x. t(x), t  T, DeclaredType(ds;x), State(ds), Consistent(R;es), R-discrete(R), b, P  Q, x:A. B(x), t.2, A c B, R-Feasible(R), f || g, False, A, P  Q, P  Q, ff, x : v, x(s), Unit, Possible(R;es), f(x), Realizer, @i: only members of L read x, @i: k sends only links in L, @i: k affects only members of L, @i (with ds: ds action a:T precondition a is P s), @i: with declarations ds:dsda:da k(v) sends f s v on link l, @i: with declarations ds:dsda:daeffect of k(v) is x := f s v, @i: only L sends on (l with tg), @i: only L affects x : t, @i: x:T initially x = v, Rrframe(loc;x;L), Rbframe(loc;k;L), Raframe(loc;k;L), Rpre(loc;ds;a;p;P), Rsends(ds;knd;T;l;dt;g), Reffect(loc;ds;knd;T;x;f), Rsframe(lnk;tag;L), Rframe(loc;T;x;L), Rinit(loc;T;x;v), left  right, Rnone(),

Lemmas

fpf-single-dom, es realizer wf, event system wf, Rrframe wf, rframe-rule, rframe-p wf, Rbframe wf, bframe-rule, bframe-p wf, Raframe wf, aframe-rule, aframe-p wf, Rpre wf, pre-rule, pre-p wf, Rsends wf, lnk wf, assert-eq-lnk, sends-rule2, sends-p wf, fpf-cap wf, isrcv wf, ma-state wf, effect-rule2, effect p wf, Reffect wf, effect p-discrete, Rsframe wf, sframe-rule2, sframe-p wf, Rframe wf, frame-rule, frame-p wf, init-rule, init p wf, Rinit wf, d-realizes-implies, init p-discrete, Rplus wf, R-compat-discrete, assert of bnot, eqff to assert, not wf, bnot wf, iff transitivity, eqtt to assert, bool sq, bool cases, fpf-join-ap-sq, fpf-join-dom, R-possible-Rplus, es-isconst wf, fpf-ap wf, top wf, fpf-trivial-subtype-top, R-discrete wf, id-deq wf, product-deq wf, fpf-dom wf, assert wf, Rnone wf, R-possible wf, bool wf, finite-prob-space wf, decl-type wf, decl-state wf, fpf wf, IdLnk wf, Knd wf, rationals wf, Id wf, unit wf